$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $L$:($T$ List), $i$:\{0..$\parallel$$L$$\parallel^{-}$\}.
\\[0ex]no\_repeats($T$;$L$) $\Rightarrow$ (index($L$;$L$[$i$]) $\sim$ $i$)